// AbstractTypeTerm.cpp : implementation file

/*#ifndef _ABSTRACTTYPETERM_CPP
#define _ABSTRACTTYPETERM_CPP

#ifdef _STDAFX_H
*/
#include "stdafx.h"
//#endif 

#include "AbstractTypeTerm.h"

//#ifndef _ABSTRACTTYPE_CPP
#include "../Types/AbstractType.h"
//#endif
/*
#ifndef _ABSTRACTTERM_CPP
#include "AbstractTerm.h"
#endif
*/
Term::pointer AbstractTypeTerm::normalized() const{
	Term::pointer NewBody = getBody().normalized();
	Term::pointer Res = new	AbstractTypeTerm(*NewBody, getVar());
	delete NewBody;
	return Res;
}
Token::pointer AbstractTypeTerm::applyArgument(Token::const_reference To) const{
	if(To.isType())
		return getBody().replaceAll(getVar(),To);
	throw Term::exception("Token::pointer TermAbstractedType::applyArgument(Token::const_reference To) const");
}

Token::pointer AbstractTypeTerm::clone()const{
      return new AbstractTypeTerm(*this);
}


bool AbstractTypeTerm::isReducible() const {
	try{
		return getBody().isReducible();
		}
	catch(Term::exception err) {
		throw err+Token::exception((string)"\r\nInvalid AbstractTypeTerm::isReducible()");	
	}
}

string AbstractTypeTerm::toString() const{
	if(this->SyntacticSugar.size()>0)
		return Token::toString();

	return string("/\\")+getVar().toString()+string(".{")+getBody().toString()+string("}");
}
string AbstractTypeTerm::view() const{
	return string("/\\")+getVar().view()+string(".{")+getBody().view()+string("}:")+
		getType().view();
	}
bool AbstractTypeTerm::operator==(Token::const_reference To)const{
	if(To.isTerm())
		if((_TERM(To)).isAbstractTypeTerm()){
			  BoundedTypeVariable TyVar("X");
			  Token::pointer Left   = this->applyArgument(TyVar);
			  Token::pointer Right = To.applyArgument(TyVar);
			  bool Res = Left->operator ==(*Right);
			  delete Left;
			  delete Right;
			  return Res;
			}
	return false;
}
Token::pointer AbstractTypeTerm::replaceAll(Token::const_reference To1, Token::const_reference To2) const{
	if(this->operator ==(To1)) return To2.clone( );
	Token::pointer NewBody = getBody().replaceAll(To1, To2);
	Token::pointer Res = new AbstractTypeTerm(_TERM(*NewBody),getVar());
	delete NewBody;
	return Res;
	}

AbstractTypeTerm::AbstractTypeTerm(const AbstractTypeTerm& Ter):
VarBody(Ter.VarBody),Term(Ter){
	
	}


AbstractTypeTerm::AbstractTypeTerm(
									   Term::const_reference Te, 
									   const AtomicType& Ty, 
									   const string& ss)
:Term(Ty, ss),VarBody(Te,Ty){

	if(Te.TypeOccursinFreeVariable(Ty))
		throw Term::exception("In AbstractTypeTerm, Type argument occurs in free variable of term");

	
	AbstractType ThisTy(Te.getType(), Ty);
	this->assignType(ThisTy);
	Token::pointer Body = Te.replaceAll(Ty,ThisTy.getVar());
	VarBody=TokenPair(ThisTy.getVar(),*Body);
	delete Body;
}


AbstractTypeTerm::~AbstractTypeTerm(){}
bool AbstractTypeTerm::TypeOccursinFreeVariable(Type::const_reference Ty) const{
	return getBody().TypeOccursinFreeVariable(Ty);
}

//#endif


